;<lemma>
; <title>SSF_pilot.2</title>
; <origin>SSF_pilot | TCTM_Ref1 | INITIALISATION/inv4/INV</origin>
(benchmark SSF_pilot_2
; <theories>
;   <theory name="linear_arith"/>
; </theories>
  :logic QF_LIA
;  <typenv>
;    <variable name="x" type="INTEGER"/>
;  </typenv>
  :extrafuns ((x Int))
  :extramacros (
		 (Nat1 (lambda (?i Int) . (<= 1 ?i)))

		 (in (lambda (?x1 't1) (?p ('t1 boolean)) . (?p ?x1)))
		 )
; <hypothesis needed="true">x : NATURAL1</hypothesis>
  :assumption (in x Nat1)
; <hypothesis needed="true">x - 1 &lt; 0</hypothesis>
  :assumption (<= (- x 1) 0)
; <goal needed="false">0 = x</goal>
  :formula
  (not
      (= x 0)
    )
)
;</lemma>
